|
In automata theory, a branch of theoretical computer science, an ω-automaton (or stream automaton) is a variation of finite automaton that runs on infinite, rather than finite, strings as input. Since ω-automata do not stop, they have a variety of acceptance conditions rather than simply a set of accepting states. ω-automata are useful for specifying behavior of systems that are not expected to terminate, such as hardware, operating systems and control systems. For such systems, one may want to specify a property such as "for every request, an acknowledge eventually follows", or its negation "there is a request which is not followed by an acknowledge". The latter is a property of infinite words: one cannot say of a finite sequence that it satisfies this property. Classes of ω-automata include the Büchi automata, Rabin automata, Streett automata, parity automata and Muller automata, each deterministic or non-deterministic. These classes of ω-automata differ only in terms of acceptance condition. They all recognize precisely the regular ω-languages except for the deterministic Büchi automata, which is strictly weaker than all the others. Although all these types of automata recognize the same set of ω-languages, they nonetheless differ in succinctness of representation for a given ω-language. ==Deterministic ω-automata== Formally, a deterministic ω-automaton is a tuple ''A'' = (''Q'',Σ,δ,''q''0,''Acc'') that consists of the following components: * ''Q'' is a finite set. The elements of ''Q'' are called the ''states'' of ''A''. * Σ is a finite set called the ''alphabet'' of ''A''. * δ: ''Q'' × Σ → ''Q'' is a function, called the ''transition function'' of ''A''. * ''q''0 is an element of ''Q'', called the initial state. * ''Acc'' is the ''acceptance condition'', formally a subset of ''Q''ω. An ''input'' for ''A'' is an infinite string over the alphabet Σ, i.e. it is an infinite sequence α = (''a''1,''a''2,''a''3,...). The ''run'' of ''A'' on such an input is an infinite sequence ρ = (''r''0,''r''1,''r''2,...) of states, defined as follows: * ''r''0 = ''q''0. * ''r''1 = δ(''r''0,''a''1). * ''r''2 = δ(''r''1,''a''2). :: ... * ''r''''n'' = δ(''r''''n''-1,''a''''n''). The main purpose of an ω-automaton is to define a subset of the set of all inputs: The set of ''accepted'' inputs. Whereas in the case of an ordinary finite automaton every run ends with a state ''r''''n'' and the input is accepted if and only if ''r''''n'' is an accepting state, the definition of the set of accepted inputs is more complicated for ω-automata. Here we must look at the entire run ρ. The input is accepted if the corresponding run is in ''Acc''. The set of accepted input ω-words is called the ''recognized ω-language'' by the automaton, which is denoted as L(A). The definition of ''Acc'' as a subset of ''Q''ω is purely formal and not suitable for practice because normally such sets are infinite. The difference between various types of ω-automata (Büchi, Rabin etc.) consists in how they encode certain subsets ''Acc'' of ''Q''ω as finite sets, and therefore in which such subsets they can encode. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Ω-automaton」の詳細全文を読む スポンサード リンク
|